$\forall$$A$:Type, $f$, $g$:$a$:$A$ fp$\rightarrow$ Top, ${\it eq}$:EqDecider($A$), $x$:$A$.
\\[0ex]($x$ $\in$ fpf{-}domain($f$ $\oplus$ $g$)) $\Leftrightarrow$ ($x$ $\in$ fpf{-}domain($f$)) $\vee$ ($x$ $\in$ fpf{-}domain($g$))